OCMon
== {g:AbMon| 
== {Linorder(|g|;x,y.(x  y))
== {& Cancel(|g|;|g|;*)
== {& (z:|g|. monot(|g|;x,y.(x  y);w.z * w))}  

latex

---

clarification:

OCMon{i}
== {g:AbMon{i}| 
== {Linorder(|g|;x,y.(x (g) y))
== {& Cancel(|g|;|g|;*g)
== {& (z:|g|. monot(|g|;x,y.(x (g) y);w.z (*g) w))}  

latex

Up	groups 1
Wellformedness Lemmas	ocmon wf
Definitions	AbMon, Linorder(T;x,y.R(x;y)), P & Q, Cancel(T;S;op), x:A. B(x), monot(T;x,y.R(x;y);f), |g|, b, , x f y, *